Lambda the Ultimate

Having been entirely too dismissive of one of Nick Benton's papers before, it seems only fitting that I should attempt expiation for my sins by discussing Formalizing and Verifying Semantic Type Soundness of a Simple Compiler:

We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple imperative language with heap-allocated data into an idealized assembly language. Types in the high-level language are interpreted as binary relations, built using both second-order quantification and a form of separation structure, over stores and code pointers in the low-level machine.

I found this work striking for its strong defense of the utility of semantic, vs. syntactic, type soundness, and for its use of logical relations vs. unary predicates. I could swear that I recently read another paper making quite similar observations about semantic vs. syntactic type soundness. I'm not sure which paper it was, but regardless, there seems to me to be a great deal of overlap of insight and, to a lesser extent, approach, with A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language, and of course by extension to Leroy's work on formalizing big-step operational semantics, allocation, etc. Finally we have the very exciting news about progress on a mechanized metatheory for Standard ML, in Twelf. It's a very exciting time for mechanized metatheory! I'd love to get at least Nick Benton, Adam Chlipala, Xavier Leroy, and Tim Sweeney in a room for a few months so they could create the Next Mainstream Programming Language in Coq. Of course, we have Dr. Benton, Mr. Chlipala, and Mr. Sweeney right here on LtU... :-)

Update: Mea culpa; the paper I had in mind was A Very Modal Model of a Modern, Major, General Type System. It would seem that Dr. Benton, Mr. Chlipala, and Dr. Appel and colleagues have arrived at quite similar perspectives on good approaches to mechanizing metatheory for very interesting programming language design efforts.

Towards a Mechanized Metatheory of Standard ML, Daniel K. Lee, Karl Crary, and Robert Harper.

We present an internal language with equivalent expressive power to Standard ML, and discuss its formalization in LF and the machine-checked verification of its type safety in Twelf. The internal language is intended to serve as the target of elaboration in an elaborative semantics for Standard ML in the style of Harper and Stone. Therefore, it includes all the programming mechanisms necessary to implement Standard ML, including translucent modules, abstraction, polymorphism, higher kinds, references, exceptions, recursive types, and recursive functions. Our successful formalization of the proof involved a careful interplay between the precise formulations of the various mechanisms, and required the invention of new representation and proof techniques of general interest.

The way that most programming languages end up working is by defining a smaller core language to which the constructions in the base language are translated. This means that you can prove the type-safety of a programming language by showing that the internal language is type safe, and that every type-correct program in the full language translates to a type-correct expression in the internal language. In this paper, the authors carried out the mechanization of a core language for SML. The next step is mechanizing the correctness of an elaborator from SML to this core language, and then full, no-foolin' SML will have a fully machine-checked correctness proof.

After reading many posts lauding interactive tools as an integral part of the next big thing in software development, I figured I could offer this as counterpoint. The paper Magic Ink: Information Software and the Graphical Interface very eloquently argues that most software today, especially information-intensive software (think IDEs and many other GUI-based PL tools) are really badly designed. The most memorable section subtitle being interactivity considered harmlful. This is a real treasure trove of wonderful design ideas for interfaces for information-rich applications.

This paper follows in the grand tradition of Edward Tufte, whose book The Visual Display of Quantitative Information was an incredible revelation for me.

Somehow, I do think that some of the ideas behind Intentional Software fit in here -- although I make no claim as to whether the actual implementation of those ideas is an appropriate realization.

Redmond, WA: At an unusual press conference held this Sunday morning, Bill Taylor, Microsoft's General Manager of Platform Strategy, announced that after much research into the causes of security holes and instabilities, Microsoft will eliminate mutable variables from the .NET platform and its languages, including C# and VB.NET. "One of our top researchers found that mutable variables were the major root cause preventing us from achieving the great user experience we always strive to deliver," said Taylor. "Once we realized that, eliminating them from .NET was a no-brainer."

Given that this announcement was made on a Sunday, reactions have been limited so far, but one prominent VB.NET developer commented that "Compared to the switch from VB6 to VB.NET, this ought to be a breeze." A C# developer was heard to say, "After anonymous delegates, monads shouldn't be a problem."

To ensure wide penetration of this significant update, Microsoft will be issuing updated Windows CDs to all licensed customers, free of charge. The new CDs can be identified by the distinctive holographic "Haskell Inside" logo, featuring a holographic version of this portrait of Simon Peyton-Jones, grinning from ear to ear.

LtU readers are encouraged to share any inside info they may have about this move!

Andreas Rossberg has updated HaMLet, a reference implementation of SML in SML, to support many of the suggestions for Successor ML (sML). The nice thing about implementing a PL in a high level PL (especially a metacircular implementation) is that it makes it easier to try out new language features.

HaMLet-S is a spin-off devoted to Successor ML (www.successor-ml.org). It incorporates a number of preliminary proposals and is a testbed and sort of a personal vision of where SML could go. Version 1.3/S4 features the following:

• Extensible records.
• More expressive pattern matching.
• Views (a la Wadler and Okasaki).
• Higher-order modules and nested signatures.
• Local and first-class modules.
• Miscellaneous fixes to known issues with SML.

A March 27, 2007 draft of a paper by Conal Elliot:

We present a user-friendly approach to unifying program creation and execution, based on a notion of “tangible values” (TVs), which are visual and interactive manifestations of pure values. Programming happens by gestural composition of TVs. Our goal is to give end-users the ability to create parameterized, composable content without imposing the usual abstract and linguistic working style of programmers. We hope that such a system will put the essence of programming into the hands of many more people, and in particular people with artistic/visual creative style.

In realizing this vision, we develop algebras for visual presentation and for “deep” function application, where function and argument may both be nested within a structure of tuples, functions, etc. Composition gestures are translated into chains of combinators that act simultaneously on statically typed values and their visualizations.

[T]his document describes a proposed ratification procedure. Discussion of this procedure is taking place on the ratification-discuss@r6rs.org mailing list. The discussion period ends on April 15th.

The Scheme Standardization Charter says that after the Editors submit a proposed final draft, "the Steering Committee should then choose either to finalize the draft or to restart the review process." This document describes how the Steering Committee will make that decision.

The ratification process proposed is somewhat unusual (e.g., a no vote will need to include an explanation), but this may change due to the comments sent to the mailing list.

I think many LtU readers should consider taking part in the vote, since as programming languages aficionados we cetainly have a stake in Scheme. Now is the chance to influence the procedural aspects of the ratification process.

Paul Cohen has passed away.

While not directly involved in programming languages, as far as I know, his seminal work in logic is certainly known and admired by many in the LtU community.

No Ifs, Ands, or Buts: Uncovering the Simplicity of Conditionals. Jonathan Edwards.

Schematic tables are a new representation for conditionals. Roughly a cross between decision tables and data flow graphs, they represent computation and decision-making orthogonally. They unify the full range of conditional constructs, from if statements through pattern matching to polymorphic predicate dispatch. Program logic is maintained in a declarative canonical form that enforces completeness and disjointness among choices. Schematic tables can be used either as a code specification/generation tool, or as a self-contained diagrammatic programming language. They give program logic the clarity of truth tables, and support high-level direct manipulation of that logic, avoiding much of the mental computation demanded by conventional conditionals.

Many of us are skeptical of "visual programming", but also intrigued by the impact that powerful development tools might have on language design. This represents an interesting compromise. It addresses a pervasive problem in a novel way, and this is a paper with many interesting and accessible ideas. I look forward to seeing an implementation.

Jonathan posted this on his blog, where there are already several comments.

[I'm not sure where to put this... Seems like plain-old "Paradigms" is the best fit...]

A Real-World Use of Lift

Well, lift is actually being used in production. I converted a Rails app to lift and it was a very interesting experience...

Then we did some benchmarking. For single request processing, the lift code, running inside Tomcat, ran 4 times faster than the Rails code running inside Mongrel. However, the CPU utilization was less than 5% in the lift version, where it was 100% of 1 CPU (on a dual core machine) for the Rails version. For multiple simultaneous requests being made from multiple machines, we're seeing better than 20x performance of the lift code versus the Rails code with 5 Mongrel instances. Once again, the lift code is not using very much CPU and the Rails code is pegging both CPUs.

In terms of new features, we've been able to add new features to the lift code with fewer defects than with the Rails code. Our Rails code had 70% code coverage. We discovered that anything shy of 95% code coverage with Rails means that type-os turn into runtime failures. We do not have any code coverage metrics for the lift code, but we have seen only 1 defect that's been checked in in the 2 weeks since we started using lift (vs. an average of 1 defect per checkin with the Rails code.)

So, yes, I'm pimping my own framework, and yes, I'm able to do with lift what guys like DHH are able to do with Rails, so the comparison is, in some ways, unfair.

On the other hand, Scala and lift code can be as brief and expressive as Ruby code. lift offers developers amazing productivity gains vs. traditional Java web frameworks, just as Rails does. On the other hand, lift code scales much better than Rails code. lift code is type-safe and the compiler becomes your friend (this does not mean you should not write tests, but it means that your tests can focus on the algorithm rather than making sure there are no type-os in variable and method names.)

I promise that "Dave Pollak" is not a pseudonym for "Paul Snively."

Update: I guess the self-deprecating humor hasn't worked, some 400+ reads later. Although the caveat that Dave offers about trying to objectively compare his own framework with Ruby on Rails is well-taken, I think that this nevertheless is an important marker in applying a very PLT-driven language and framework, Scala and lift, to a very realistic application, especially given that it's a rewrite from a currently-popular language and framework, Ruby and Rails. We admitted proponents of static typing and weird languages are constantly being asked for this sort of thing, and while it's doubtful that this adds anything to the PLT discussion per se—at least until we have a chance to dig into lift and see how Scala's design uniquely supports it—I thought people might find the Scala connection worth commenting on.